L:MsgA List, l:IdLnk, tg:Id.
(A,BL.A ||+ B)  (rcv(l,tg) declared in (L)  (ML.rcv(l,tg) declared in M)) 

latex

Definitions	{T}, M1 || M2, M1  M2, M1 ||decl M2, P  Q, x,y. t(x;y), (x,yL.P(x;y)), , rcv(l,tg) declared in M, (xL.P(x)), mk-ma, (x  l), P  Q, P  Q, b, x  dom(f), KindDeq, rcv(l,tg), Prop, A ||+ B, l[i], {i..j}, i  j < k, ||as||, Id, IdLnk, P & Q, x:A. B(x), A & B, , AB, A, False, P  Q, 1of(t), Valtype(da;k), a:A fp B(a), x. t(x), Knd, x:A. B(x), t  T, MsgA, (L)
Lemmas	msga wf, Knd wf, fpf-trivial-subtype-top, IdLnk wf, Id wf, length wf2, select wf, ma-compat wf, int seg wf, rcv wf, Kind-deq wf, fpf-dom wf, assert wf, nat wf, false wf, pairwise-cons, pairwise wf, l exists wf, ma-join-list wf, ma-declm wf, ma-join wf, ma-join-declm, iff functionality wrt iff, ma-join-list-compat, l exists cons